| Definitions | Type, False, MaInterface(T), (x  l), x:A  B(x),  x:A. B(x), s = t, {T}, x:A  B(x), P   Q,  x:A. B(x), SQType(T),  , strong-subtype(A;B), s ~ t, left + right,  , #$n,  , ff, Void, True, Unit, ma-interface-loc(I;i), {x:A| B(x)} , Knd, State(ds), hasloc(k;i),  x.A(x),  x. t(x), Atom$n, a < b, ma-interface-locs(I), ma-interface-dom(I;i), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , type List, S  T, Outcome, A  B, ||as||,  A,  , l[i], |g|, A c B, P & Q, P  Q, [car / cdr], P  Q, P Q, hd(l), last(L),  , IdDeq, x dom(f),  b, Top, Id, a:A fp B(a), t T, null(as),  b, tt,  x:A.B(x), <a, b>, i <z j, i z j, n+m, i j < k, i  j , {i..j },  , IdLnk, p =b q, (i = j), x =a y, a < b, f(a), x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), p q, p q, p q, [], tl(l), n - m, if a<b then c else d, nth_tl(n;as), rec-case(a) of [] => s | x::y => z.t(x;y;z), Y, Dec(P), b | a, a ~ b, a b, a <p b, a < b, xL. P(x), (xL.P(x)), r s, r < s, q-rel(r;x), l_disjoint(T;l1;l2), (e <loc e'), e loc e' , (e < e'), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), es-r-immediate-pred(es;R;e';e), same-thread(es;p;e;e'), [e: i p j], [e: i  p j], f2f+-pred(e',e), fpf-domain(f), EqDecider(T) |